\begin{tabbing}
$\forall$$T$:Type, ${\it as}$:($T$ List), $f$,$g$:($T$$\rightarrow\mathbb{B}$).
\\[0ex]((priority{-}select($f$; $g$; ${\it as}$) = (inl tt ) $\in$ (?$\mathbb{B}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$$i$:int\_seg(0; $\parallel$${\it as}$$\parallel$). (($\uparrow$($f$(${\it as}$[$i$]))) $\wedge$ ($\forall$$j$:int\_seg(0; $i$). $\neg$($\uparrow$($g$(${\it as}$[$j$])))))))
\\[0ex]$\wedge$ \=((priority{-}select($f$; $g$; ${\it as}$) = (inl ff ) $\in$ (?$\mathbb{B}$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$$i$:int\_seg(0; $\parallel$${\it as}$$\parallel$). (($\uparrow$($g$(${\it as}$[$i$]))) $\wedge$ ($\forall$$j$:int\_seg(0; ($i$ + 1)). $\neg$($\uparrow$($f$(${\it as}$[$j$])))))))
\-\\[0ex]$\wedge$ \=((priority{-}select($f$; $g$; ${\it as}$) = (inr $\cdot$ ) $\in$ (?$\mathbb{B}$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\forall$$i$:int\_seg(0; $\parallel$${\it as}$$\parallel$). ($\neg$($\uparrow$($f$(${\it as}$[$i$])))) $\wedge$ ($\neg$($\uparrow$($g$(${\it as}$[$i$]))))))
\-
\end{tabbing}